CTF Re

2023-09-28 01:38| 来源: 网络整理| 查看: 265

一安装：

z3是由微软公司开发的一个优秀的SMT求解器（也就定理证明器），它能够检查逻辑表达式的可满足性。

我是在windows下pyCharm 里面自己添加包包名为z3-slover（不是z3）

二使用：

库内函数：

1.创建一个解的声明对象：

s = Solver()

2.添加条件：

s.add(判断公式)

3.判断是否有解：

s.check()

如果有解则反回sate/sat 反之返回 unsate/unsat

4.返回最后的解：

result=s.modul() print(result)

5.声明不同类型的未知数：

a, s, d = Ints('a s d')#创建一个‘int’类型的对象，但其实运算时候是'ArithRef'类型， #并且无法使用按位运算 x = Real('x') #创建一个有理数类型的变量。 y = Real('y')

z3库最牛逼的来了:上面两个就是比正常多元未知数复杂了点，求解按位运算才是这个库最吊的！

BitVecs(name,bv,ctx=None),创建一个有多变量的位向量，name是名字，bv表示大小 #a,b,c=s=BitVecs('a b c',32) Bitvex(name,bv,ctx=None),创建一个位向量，name是他的名字，bv表示大小 BitVecSort(bv,ctx=None),创建一个指定大小的位向量 BitVecVal(val,bv,ctx=None),创建一个位向量，有初始值，没名字

三：例题

大概使用流程：

from z3 import * a, b, c=BitVecs('a b c',32) d, e, f=BitVecs('d e f',32) g, h, i=BitVecs('g h i',32) key=[a,b,c,d,e,f,g,h] s = Solver() s.add() check = s.check() print(check) model = s.model() print(model)

四:CTF逆向的使用

对于一些较为复杂的算法，我们很难逆向或者爆破求出他的最终结果，这时可以使用z3库正向帮助我们解决问题。

特殊代码

X = [BitVec(('x%s' % i),8) for i in range(0x22) ] 声明一个列表，数据类型是向量，形式是 xi，向量的大小是8

[x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33]

.as_long()函数可以把z3库里面特殊的类型转换成long类型

例如： res.append(chr(m[flag[i]].as_long()))

例题：第八届极客大挑战REConvolution

关键代码：

int __cdecl main(int argc, const char **argv, const char **envp) { unsigned int ii; // esi unsigned int v4; // kr00_4 char flag_i; // bl unsigned int jj; // eax char *v7; // edx char v8; // cl int v9; // eax char xor_result[80]; // [esp+8h] [ebp-A4h] char flag[80]; // [esp+58h] [ebp-54h] sub_DC1020("Please input your flag: "); sub_DC1050("%40s", flag); memset(xor_result, 0, 0x50u); ii = 0; v4 = strlen(flag); if ( v4 ) { do { flag_i = flag[ii]; jj = 0; do { v7 = &xor_result[jj + ii]; v8 = flag_i ^ data1[jj++]; *v7 += v8; } while ( jj < 0x20 ); ++ii; } while ( ii < v4 ); } v9 = strcmp(xor_result, (const char *)&data2); if ( v9 ) v9 = -(v9 < 0) | 1; if ( v9 ) puts("No, it isn't."); else puts("Yes, it is."); return 0; }

逆向很难求解，我们试试z3正向求解。

from z3 import * s = Solver() X = [BitVec(('x%s' % i),8) for i in range(0x22) ] print (X) data1 = [0x21,0x22,0x23,0x24,0x25,0x26,0x27,0x28,0x29,0x2A,0x2B,0x2C,0x2D,0x2E,0x2F,0x3A, 0x3B,0x3C,0x3D,0x3E,0x3F,0x40,0x5B,0x5C,0x5D,0x5E,0x5F,0x60,0x7B,0x7C,0x7D,0x7E] data2 = [0x72,0xE9,0x4D,0xAC,0xC1,0xD0,0x24,0x6B,0xB2,0xF5,0xFD,0x45,0x49,0x94,0xDC,0x10, 0x10,0x6B,0xA3,0xFB,0x5C,0x13,0x17,0xE4,0x67,0xFE,0x72,0xA1,0xC7,0x04,0x2B,0xC2, 0x9D,0x3F,0xA7,0x6C,0xE7,0xD0,0x90,0x71,0x36,0xB3,0xAB,0x67,0xBF,0x60,0x30,0x3E, 0x78,0xCD,0x6D,0x35,0xC8,0x55,0xFF,0xC0,0x95,0x62,0xE6,0xBB,0x57,0x34,0x29,0x0E,3] xor_result = [0]*0x41 for m in range(0,0x22): for n in range(0,0x20): xor_result[n+m] += X[m] ^ data1[n] for o in range(0,0x41): s.add(xor_result[o] == data2[o]) print (s.check()) m = s.model() print("traversing model...") flag='' for i in range(0,0x22): flag+=chr(int("%s" % (m[X[i]]))) print(flag)

【本文地址】

公司简介

联系我们